Compilers transform programs from high-level programming languages to machine code by a series of steps. At each stage in compilation, an intermediate language can be defined to represent programs at that stage. At each new stage, the corresponding intermediate language representation exposes more details of the computation than the previous stage up to the point where machine code is reached. Maintaining information regarding types within such intermediate representations has significant benefits. For instance, a typed intermediate language allows intermediate program representations to be type-checked and, thus, can be used to debug compilers, to guide optimizations, and to generate safety proofs for programs. Furthermore, typed intermediate representations can be used as a format for redistributing programs and a user can (mechanically) check that the program redistributed in the intermediate form is safe to run, as opposed to relying on certificates or third party claims of trustworthiness.
In practice, however, compilers for object-oriented languages do not maintain enough type information in low-level intermediate representations so programs in those representations can be typechecked, even though their input is statically typed. One reason, compilers for object-oriented languages have failed to adopt compilation using typed intermediate representations is the complexity related to the traditional class and object encodings used in previous approaches to obtaining typed intermediate representations for object-oriented languages compilation methods. A great deal of work has been done for developing typed intermediate languages for functional languages, but much of this work does not support object-oriented programming languages, which are widely used in practice (e.g., C#, C++, and JAVA. JAVA is a trademark of Sun Microsystems, Inc.). Thus far, those typed intermediate languages that have been proposed for object-oriented languages are complicated, often inefficient, and do not allow compilers to use standard implementation techniques. In short, they are not suitable for practical compilers.
A practical compiler requires simple, general, and efficient type systems. First, compiler writers who are not type theorists should be able to understand the type system. Second, the type system needs to cover a large set of realistic object-oriented language features and compiler transformations. Third, the type system needs to express standard implementation techniques without introducing extra runtime overhead. To enable any of the above at the intermediate language level, methods and systems are needed to maintain type information in the intermediate language compiled from a source code representation.